THE INPUT FORMULA
The specification is:
{L0}:[-1]:BUTTON1(x1) +0 < [-1]:StartRA1(x1)
{L1}:[-1]:StartRA1(x2) +40 < [-1]:StopRA1(x2)
{L2}:[-1]:StopRA1(x3) +0 < [-1]:GRANT1true(x3)
{L3}:[-1]:GRANT1true(x4) +0 < [-1]:StartMOVE1(x4)
{L4}:[-1]:StartMOVE1(x4) -5 < [-1]:GRANT1true(x4)
{L5}:[-1]:StopMOVE1(x6) -20 < [-1]:StartMOVE1(x6)
{L6}:[-1]:BUTTON2(x7) +0 < [-1]:StartRA2(x7)
{L7}:[-1]:StartRA2(x8) +40 < [-1]:StopRA2(x8)
{L8}:[-1]:StopRA2(x9) +0 < [-1]:GRANT2true(x9)
{L9}:[-1]:GRANT2true(x10) +0 < [-1]:StartMOVE2(x10)
{L10}:[-1]:StartMOVE2(x10) -5 < [-1]:GRANT2true(x10)
{L11}:[-1]:StopMOVE2(x12) -20 < [-1]:StartMOVE2(x12)
{L12}:[-1]:GRANT1true(x5) +30 < [-1]:GRANT1false(x5)
{L13}:[-1]:GRANT2true(x11) +30 < [-1]:GRANT2false(x11)
{L14}:[-1]:GRANT1false(x13) +0 < [-1]:GRANT2true(x14) OR {L15}:[-1]:GRANT2false(x14) +0 < [-1]:GRANT1true(x13)
The safety assertion is:
{L16}:[-1]:StartMOVE1(I) +0 < [-1]:StopMOVE2(J)
{L17}:[-1]:StartMOVE2(J) +0 < [-1]:StopMOVE1(I)

THE UNOPTIMIZED FORMULA
The specification is:
{L0}:[0]:BUTTON1(x1) +0 < [1]:StartRA1(x1)
{L1}:[2]:StartRA1(x2) +40 < [3]:StopRA1(x2)
{L2}:[4]:StopRA1(x3) +0 < [5]:GRANT1true(x3)
{L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4)
{L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4)
{L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6)
{L6}:[10]:BUTTON2(x7) +0 < [11]:StartRA2(x7)
{L7}:[12]:StartRA2(x8) +40 < [13]:StopRA2(x8)
{L8}:[14]:StopRA2(x9) +0 < [15]:GRANT2true(x9)
{L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10)
{L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10)
{L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12)
{L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5)
{L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11)
{L14}:[24]:GRANT1false(x13) +0 < [25]:GRANT2true(x14) OR {L15}:[26]:GRANT2false(x14) +0 < [27]:GRANT1true(x13)
The safety assertion is:
{L16}:[28]:StartMOVE1(I) +0 < [29]:StopMOVE2(J)
{L17}:[30]:StartMOVE2(J) +0 < [31]:StopMOVE1(I)
The set of positive cycles:
NOT {L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) OR NOT {L16}:[28]:StartMOVE1(I) +0 < [29]:StopMOVE2(J) OR NOT {L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) OR NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) OR NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[26]:GRANT2false(x14) +0 < [27]:GRANT1true(x13)
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[24]:GRANT1false(x13) +0 < [25]:GRANT2true(x14) OR NOT {L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) OR NOT {L17}:[30]:StartMOVE2(J) +0 < [31]:StopMOVE1(I) OR NOT {L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) OR NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4)
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[24]:GRANT1false(x13) +0 < [25]:GRANT2true(x14) OR NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[26]:GRANT2false(x14) +0 < [27]:GRANT1true(x13)

The determinant of the unoptimized formula:0.0 (so the real-time specification implies the safety assertion)

THE OPTIMIZED FORMULA
The specification is:
{L0}:[0]:BUTTON1(x1) +0 < [1]:StartRA1(x1)
{L1}:[2]:StartRA1(x2) +40 < [3]:StopRA1(x2)
{L2}:[4]:StopRA1(x3) +0 < [5]:GRANT1true(x3)
{L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4)
{L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4)
{L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6)
{L6}:[10]:BUTTON2(x7) +0 < [11]:StartRA2(x7)
{L7}:[12]:StartRA2(x8) +40 < [13]:StopRA2(x8)
{L8}:[14]:StopRA2(x9) +0 < [15]:GRANT2true(x9)
{L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10)
{L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10)
{L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12)
{L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5)
{L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11)
{L14}:[24]:GRANT1false(x13) +0 < [25]:GRANT2true(x14) OR {L15}:[26]:GRANT2false(x14) +0 < [27]:GRANT1true(x13)
The safety assertion is:
{L16}:[28]:StartMOVE1(I) +0 < [29]:StopMOVE2(J)
{L17}:[30]:StartMOVE2(J) +0 < [31]:StopMOVE1(I)
The set of positive cycles:
NOT {L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) OR NOT {L16}:[28]:StartMOVE1(I) +0 < [29]:StopMOVE2(J) OR NOT {L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) OR NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) OR NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[26]:GRANT2false(x14) +0 < [27]:GRANT1true(x13)
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[24]:GRANT1false(x13) +0 < [25]:GRANT2true(x14) OR NOT {L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) OR NOT {L17}:[30]:StartMOVE2(J) +0 < [31]:StopMOVE1(I) OR NOT {L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) OR NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4)
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[24]:GRANT1false(x13) +0 < [25]:GRANT2true(x14) OR NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[26]:GRANT2false(x14) +0 < [27]:GRANT1true(x13)

The determinant of the optimized formula: 0.0 (so the real-time specification implies the safety assertion)